
{--
    Heart of the code generation.
    
    Determination of appropriate java types and conversions between lazy, strict, known
    and unknown values.
    
    -}

module frege.compiler.gen.java.Bindings
        -- inline (adaptSigma, adaptSigmaWith) 
    where

import frege.Prelude hiding(<+>)

import Data.TreeMap (TreeMap Map)
-- import Data.List as DL(zip4)
import Data.Bits(BitSet.member)


-- import  Compiler.common.Errors as E()
-- import  frege.lib.PP hiding(group, break, line)
-- import  Compiler.types.Positions
-- import  Compiler.enums.Flags(TRACEZ)

-- import  Compiler.Utilities as U()
import  Compiler.Javatypes(subTypeOf)
import  Compiler.gen.java.Common

import  Compiler.enums.RFlag(RValue)

import  Compiler.common.Roman(romanUpper)

import  Compiler.types.AbstractJava
import  Compiler.types.Strictness
import  Compiler.types.JNames(memberOf, JName)
import  Compiler.types.Types
-- import  Compiler.types.Symbols
import  Compiler.types.ConstructorField(Field, ConField)
import  Compiler.types.QNames(QName)
import  Compiler.types.Global as G

import  Compiler.classes.Nice(Nice)
import  Compiler.enums.Flags(isOn, TRACEG)


{--
 * This data structure describes java compile time types
 * of some frege item (argument, return value, field, expression) 
 * and java expression associated with it.
 * 
 * The task of code generation is to create, combine and
 * manipulate such bindings. Many code generating functions will take
 * a ('Tree' 'Symbol' 'Binding') of current bindings as last parameter.
 -}
data Binding = Bind {?stype :: String, !ftype::Sigma, !jtype :: JType, !jex :: JExpr}
instance Show Binding where
    show (Bind {stype, jtype, jex}) = "Bind {" 
                                            ++ stype ++ ", "
                                            ++ show jtype ++  ", "
                                            ++ showJex jex ++ "}"

newBind g sigma jex = Bind{stype=nicer sigma g, 
                        ftype=sigma, jtype=sigmaJT g sigma, jex}

--- tell if the item we are working with is strict  
isStrictJT :: JType -> Bool
isStrictJT Lazy{yields}          = false
isStrictJT _                     = true

--- tell if the item we are working with is known
isKnownJT :: JType -> Bool
isKnownJT Something             = false
isKnownJT Lazy{yields}          = isKnownJT yields
isKnownJT _                     = true



{--
    - If the 'RAlways' flag is set, the return type will always be @Lazy@
    - If the 'RValue' flag is on, the return type will be @int@, @String@ or @TList@
    - Otherwise, lazy as well as non lazy results may be returned. For native types, 
      this means the return type is @Something@. Frege types are returned as @Lazy@.
-}
returnType mode rjt = if RValue `member` mode 
    then strict rjt
    else lazy rjt

{--
    convert an arg quadrupel to a 'Binding'
    -}
arg2Bind g = quadBind g JAtom 

quadBind g f (_, sig, jt, s) = Bind (nicer sig g) sig jt (f s)

{--
     Adapt a 'Binding' to the required strictness and target type.
    --}
adaptBind :: Global -> Binding -> Strictness -> Binding
adaptBind g bind s
     = adaptLazinessWith (if Strictness.isStrict s then strict else lazy) g bind
        
 
--- adapt argument to wanted strictness
adaptArg g a s = adaptBind g (arg2Bind g a) s

--- instantiate 'Binding' for an Argument
instArg = arg2Bind

--- Invoke method with single argument
invokeSingle meth arg = JInvoke meth [arg]


--- force a lazy 'Binding'
force :: Binding -> Binding
force Bind{stype, ftype, jtype = Lazy{yields}, jex}
                    = Bind{stype, ftype, jtype = boxed yields, 
                            jex = JInvoke JExMem{jex, name="call", targs=[]} []}

force bind 
    = error("unneeded force: " ++ show bind)

--- Force a lazy @bind@ and give it type @to@
--- This is only possible for 'Bindings' having type @Lazy Something@
forceTo :: Binding -> JType -> Binding
forceTo bind to
    | Lazy Something <- bind.jtype = (force bind).{jtype=to, jex <- JCast to}
    | otherwise = error("cannot forceTo: " ++ show bind ++ " to " ++ show to)

     
{-- 
    Delay a 'Binding' by wrapping it in a Lazy lambda, see 'lazyIt'

    -}
delay :: Binding -> Binding
delay bind = bind.{jex ← lazyIt bind.jtype, jtype ← lazy}


{-- 
    coerce Kinded<T<A,B,C,?,...>,D,...> to T<A,B,C,D,...>

    The name of the coerce function for functions is @Func.coerceX@
    where X is the roman number of the arity,
    otherwise just T.coerce
-}
coerceKinded g Bind{stype, ftype, jtype, jex} = case jtype of
    Kinded{arity,gargs = un:args} -> case un of
        Func{gargs} → Bind{stype, ftype, jtype = target, jex = coex}
            where
                target = Func (take (farity - arity) gargs ++ args)
                name   = "coerce" ++ romanUpper (farity - 1)
                smem   = JX.staticMember (JName (targetName g "Func") name)
                gmem   = smem.{targs = target.gargs}
                coex   = JInvoke gmem [jex] 
                farity = length gargs
        Nativ{} → Bind{stype, ftype, jtype = fromKinded jtype, jex}
        TArg{}  → Bind{stype, ftype, jtype = un, jex = JCast un jex} 
        other = case other.{gargs?} of
            true = Bind{stype, ftype, jtype = target, jex = coex}
                where
                    tarity = length other.gargs
                    target = other.{gargs = take (tarity - arity) other.gargs ++ args}
                    gmem   = JX.static "coerce" target
                    coex   = JInvoke gmem [jex]
            _ -> error ("coerceKinded no suitable target type: " ++ show jtype)
    _ -> error ("coerceKinded argument not kinded: " ++ show jtype)



infixl 5 adapt  
{--
    Adapt a binding to a given target type

    Note that all adaptions should be justified through type checking.
    In particular, we are not doing exhaustive Java type checking here.

    If the conversion is undefined, this hints at a compiler error.
    -}
adapt ∷ Global → Binding → JType → Binding
adapt g bind1 toType = case adaptQ g bind1 toType of
    Right newb      → newb
    Left (bind, from, to) → if try from to 
                        then case bind.jtype of
                            Ref{}
                                | Kinded{} ← toType, Kinded{} ← to = higher
                                | toType.{gargs?} 
                                  → bind.{jtype = toType, 
                                           jex = JX.invoke [] (
                                                 JExMem{jex=bind.jex, 
                                                        name="simsalabim", 
                                                        targs = toType.gargs}
                                            )}
                            Func{gargs = [a@Nativ{}, _]} 
                                    |  Func{gargs = [c@Nativ{}, _]} ← toType, a.typ != c.typ,
                                       subTypeOf g c.typ a.typ
                                    = bind.{jtype = toType, jex ← flip convertHigher toType}
                            -- the following is common in IO stuff, where some constructor returns
                            -- for example a FileInputStream, but the consuming functions 
                            -- take the more general InputStream
                            Func{gargs = [_, a@Nativ{}]} 
                                    |  Func{gargs = [_, b@Nativ{}]} ← toType, a.typ != b.typ,
                                       subTypeOf g a.typ b.typ
                                    = bind.{jtype = toType, jex ← flip convertHigher toType}
                            -- try some magic inside the function
                            Func{} | -- JCast{jt=Func{}, jex=lam@JLambda{}} <- bind.jex,
                                     Kinded{} ← to, -- there is a Kinded function in the target somewhere
                                     Just nex <- lambdaToKinded toType bind.jex
                                   =  bind.{jtype = toType, jex = nex}
                                   | Kinded{} ← to      = higher
                                   | Kinded{} ← from    = higher
                                   | Something ← to     = higher
                                   | Something ← from   = higher
                            Kinded{}
                                   | Kinded{} ← to      = higher    -- to kinded in type argument 
                            report | isOn g.options.flags TRACEG, traceLn("DOUBLE CASTING  "
                                        ++ show bind 
                                        ++ "\nTO  " 
                                        ++ show toType
                                        ++ "\nBECAUSE  "
                                        ++ show from
                                        ++ "  DOES NOT MATCH  "
                                        ++ show to) = undefined
                            -- last resort
                            -- this will probably work too, but triggers "Unchecked" warning
                            other → bind.{jtype = toType, jex ← JCast toType . JCast Something}

                        else  error ("Can't adapt\n" 
                                ++ show bind 
                                ++ "\nto  " 
                                ++ show toType
                                ++ "\nbecause  "
                                ++ show from
                                ++ "  does not match  "
                                ++ show to)
        where
            -- cast via RunTM.cast
            higher = bind.{jtype = toType, jex = convertHigher bind.jex toType}
            -- go down a chain of functions and change Func{} to Kinded{} accordingly
            -- lambdaToKinded _ _ = Nothing
            lambdaToKinded to ex = case (to, ex) of
                (Kinded{}, JCast _ ex) = Just (JCast to (JCast Something ex))
                (Kinded{}, ex) = Just (JCast to (JCast Something ex))
                (Func{gargs=[_,next]}, JCast Func{} JLambda{fargs, code})
                    | Left cex  ←  code             -- try next level
                    = case lambdaToKinded next cex of
                        Just nex → Just ex.{jex ← _.{code = Left nex}, jt=to}
                        _        → Nothing
                (Func{}, JAtom{}) = Just (convertHigher ex to)
                _   → Nothing
            try Something _ = true
            try _ Something = true
            try from to = case from of
                Nativ{} | Nativ{} ← to = true
                Wild{} = true
                Kinded{}
                    | canBeKinded to from.arity
                    = case unifyJT (fromKinded from) to Map.empty of
                                     Right _    → true
                                     Left (f,t) | f!=from, t!=to → try f t
                                                | otherwise = false
                    -- Kinded{} ← to = try (fromKinded from) to 
                    | otherwise     = false
                _ = case to of
                    Wild{} = true 
                    Kinded{} 
                        | canBeKinded from to.arity
                        =  case unifyJT from (fromKinded to) Map.empty of
                                     Right _    → true
                                     Left (f,t) | f!=from, t!=to → try f t
                                                | otherwise = false
                        | otherwise  = false
                    _   = false


adaptQ g bind toType
    = case unifyJT bind.jtype toType Map.empty of 
        Right _  = accept
        -- Left _ | traceLn("adapt " ++ show bind.jtype ++ "  to  " ++ show toType) = undefined
        Left (f1, f2) = case bind.jtype of
            Lazy{yields}
                        = case toType of
                            -- the following maps `adapt` over Lazy
                Lazy{}      = Right (delayBind (adapt g forced toType.yields)) 
                                --case adaptQ g forced toType.yields of
                                --    Left (_, f1, f2) → Left (bind, f1, f2)
                                --    Right b → Right (delayBind b)
                _           = adaptQ g forced toType
            Kinded{}    = case toType of
                Lazy to     = ensureLazy <$> adaptQ g bind to
                Kinded{}    = cannot f1 f2
                _           = adaptQ g unkinded toType
            Nativ{}
                | Just _ ←  isPrimitive bind.jtype, Nothing ← isPrimitive toType
                            = adaptQ g boxit toType
                | Nothing ← isPrimitive bind.jtype, Just _ ←  isPrimitive toType
                            = adaptQ g unboxed toType
                | Nativ{} ← toType = casted     -- downcast
            nonlazy     = case toType of
                Lazy to     = ensureLazy <$> adaptQ g bind to
                Kinded{arity} 
                    | canBeKinded nonlazy arity,
                      Right _ <- unifyJT (asKinded nonlazy arity) toType Map.empty
                    = casted 
                Something   = accept 
                _           = cannot f1 f2
            -- _           = cannot
          where cannot f1 f2
                    -- | traceLn("cannot: from " ++ show f1 ++ " to " ++ show f2) || true   
                    = Left (bind, f1, f2)

    where
        unboxed  = bind.{jtype = p, jex ← JCast p}
                    where p = strict bind.jtype
        boxit    = bind.{jtype ← boxed}
        accept   = Right bind.{jtype = toType}
        casted   = Right bind.{jtype = toType, jex ← JCast toType}
        forced   = force bind
        unkinded = coerceKinded g bind

--- make sure the binding can be passed as Lazy 
ensureLazy :: Binding → Binding
ensureLazy bind  = case bind.jtype  of
    Lazy{yields}            →  bind 
    Constr{jname, gargs}    →  error ("Can't lazy a constraint " ++ show bind)
    t | implementsLazy t    →  bind.{jtype ← lazy}
    other                   →  bind.{jex ← lazyJX bind.jtype, jtype ← lazy} 

delayBind ∷  Binding → Binding 
delayBind bind = bind.{jex ← thunkIt bind.jtype . Left, jtype ← lazy}

    
--- make sure a strict binding actually is primitive if type allows
primitiveBind g bind
    | Nativ{} <- sbind.jtype,
      prim != sbind.jtype       = sbind.{jtype = prim, jex <- JX.cast prim}
    | otherwise                 = sbind
    where
        sbind = strictBind g bind
        prim  = strict sbind.jtype
 

---    make a binding strict
strictBind ∷ Global → Binding → Binding
strictBind g bind = adapt g bind (strict bind.jtype)

---    make a binding lazy
lazyBind ∷ Global → Binding → Binding
lazyBind g bind = adapt g bind (lazy bind.jtype)

adaptLazinessWith f g bind = adapt g bind (f bind.jtype)
-- adaptSigma       g bind = adapt g bind (  (sigmaJT g bind.ftype))

{--
    [usage] @realize bind@

    code to create a local variable and an updated bind
    -}
realize :: String -> Binding -> StG (Binding, [JStmt])
realize name bind
    | cheap (Binding.jex bind) = do
        g <- getST
        stio (bind, [sComment ("too cheap to realize " ++ name ++ " bound to " ++ show bind)])
    | otherwise = do
        u <- uniqid
        g <- getST
        let vname = m name -- ++ underline ++ show u  -- must correspond to U.javaName
            m "$" = "$" ++ show u
            m s   = s
            member = JMember {attr = attrFinal,
                            jtype = Binding.jtype bind,
                            name = vname,
                            init = Just (Binding.jex bind)}
            nbind = bind.{jex = JAtom vname}
        stio (nbind, 
                [sComment ("realize " ++ name ++ " bound to " ++ show bind), 
                 JLocal member])

assign :: Global -> ConField QName -> FormalArg -> JStmt
assign g Field{pos, name = Just toname, doc, vis, strict, typ} formalArg  
        = JAssign (JAtom toname) bind.jex
    where
        bind   = adaptArg g formalArg (if strict then S[] else U)
assign g f a = error "assign: apply only named fields here"     -- see namedFields
